T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:es-E(es).
es-dtype(es; loc(e); x; T)
 (e':es-E(es). 
 ((x changed before e) c ((last change to x before e) = e'))
  (es-locl(es; e'; e)
   ((es-after(es; x; e') = es-when(es; x; e')  T))
   (e'':es-E(es). 
   es-locl(es; e'; e'')
    es-locl(es; e''; e)
    (es-after(es; x; e'') = es-when(es; x; e'')  T)))) 

latex

Definitions	prop{i:l}, t  T, P  Q, P  Q, A c B, P  Q, P  Q, x:A. B(x), es-locl(es; e; e'), guard(T), sq_type(T), True, T, A, False, es-dtype(es; i; x; T), P  Q
Lemmas	es-when wf, es-vartype wf, es-loc-pred, es-after wf, not wf, es-causl wf, last-change wf, es-loc wf, es-dtype wf, changed wf, assert wf, es-locl wf, es-locl-iff, last-change-property, es-le weakening, es-locl transitivity2, es-pred-locl, bool wf, bool sq, event system wf, es-E wf, true wf, squash wf, es-after-pred2